The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X), YS) → cons(X)
from(X) → cons(X)
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X), cons(Y)) → cons(app(Y, cons(X)))
prefix(L) → cons(nil)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0
app(cons(z0), z1) → cons(z0)
from(z0) → cons(z0)
zWadr(nil, z0) → nil
zWadr(z0, nil) → nil
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0)))
prefix(z0) → cons(nil)

Tuples:

ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))

S tuples:

ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))

K tuples:none
Defined Rule Symbols:

app, from, zWadr, prefix

Defined Pair Symbols:

ZWADR

Compound Symbols:

c5

(3) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 1 dangling nodes:

ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0
app(cons(z0), z1) → cons(z0)
from(z0) → cons(z0)
zWadr(nil, z0) → nil
zWadr(z0, nil) → nil
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0)))
prefix(z0) → cons(nil)

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

app, from, zWadr, prefix

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))